Nuprl Lemma : ma-sub-join-list 0,22

L:MsgA List, M:MsgA. (A,BL.A ||+ B (M  L M  (L
latex


DefinitionsM1 || M2, M1 ||decl M2, M1  M2, x,yt(x;y), P  Q, P  Q, (x,yL.P(x;y)), Prop, A ||+ B, l[i], {i..j}, i  j < k, AB, P & Q, A, False, P  Q, ||as||, (x  l), x:AB(x), A & B, M1  M2, , x:AB(x), t  T, MsgA, (L)
Lemmasmsga wf, length wf2, select wf, ma-compat wf, int seg wf, l member wf, cons member, pairwise-cons, pairwise wf, ma-join-list wf, ma-join wf, ma-sub wf, ma-sub-join-left, ma-join-list-property, ma-sub transitivity, ma-sub-join-right

origin